Using Animation in Diagrammatic Theorem Proving

摘要

Diagrams have many uses in mathematics, one of the most ambitious of which is as a form of proof. The domain we consider is real analysis, where quantification issues are subtle but crucial. Com- puters offer new possibilities in diagrammatic reasoning, one of which is animation. Here we develop animated rules as a solution to problems of quantification. We show a simple application of this to constraint di- agrams, and also how it can deal with the more complex questions of quantification and generalisation in diagrams that use more specific rep- resentations. This allows us to tackle difficult theorems that previously could only be proved algebraically.